T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:{e:es-E(es)| es-dtype(es; loc(e); x; T)} .
(x changed before e)  ((last change to x before e)  es-E(es)) 

latex

Definitions	Type, t  T, x:A. B(x), EqDecider(T), event_system{i:l}, Id, loc(e), es-dtype(es; i; x; T), es-E(es), {x:A| B(x)} , change-to(x;e), Unit, isl(x), b, P  Q, outl(x), (last change to x before e), x changed before e
Lemmas	outl wf, assert wf, isl wf, unit wf, change-to wf, es-E wf, es-dtype wf, es-loc wf, Id wf, event system wf, deq wf